$\forall$$A$:MsgA, $l$:IdLnk, $k$:Knd, $s$:$A$.state, $v$:$A$.da($k$).
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ $\neg$$A$.bframe($k$ sends on $l$)
\\[0ex]$\Rightarrow$ filter($\lambda$${\it ms}$.mlnk(${\it ms}$) = $l$;$A$.sends($k$,$s$,$v$)) $=$ nil $\in$ $A$.Msg List